\begin{tabbing}
$\forall$\=${\it ds}$:$x$:Id fp$\rightarrow$ Type, ${\it da}$:$k$:Knd fp$\rightarrow$ Type, $v$:ecl{-}trans{-}tuple\{i:l\}(${\it ds}$;${\it da}$),\+
\\[0ex]$L$:(event{-}info(${\it ds}$;${\it da}$) List), $x$:($v$.1). ecl{-}trans{-}reachable(${\it ds}$;${\it da}$;$v$;$L$;$x$) $\in$ $\mathbb{P}$
\-
\end{tabbing}